/*    This file is part of rls.
 *
 *    Rls is free software: you can redistribute it and/or modify
 *    it under the terms of the GNU Lesser General Public License as published by
 *    the Free Software Foundation, either version 3 of the License, or
 *    (at your option) any later version.
 *
 *    Rls is distributed in the hope that it will be useful,
 *    but WITHOUT ANY WARRANTY; without even the implied warranty of
 *    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *    GNU Lesser General Public License for more details.
 *
 *    You should have received a copy of the GNU Lesser General Public License
 *    along with rls.  If not, see <http://www.gnu.org/licenses/>.
 */

#include <rid.h>
#include <stdint.h>
#include <stdlib.h>
#include <unistd.h>

#define STYLE_9
#include <unfy/unfy.h>

#include "rls.h"

/* utility code for binds */

#define ARRAY_UNITS(array) (sizeof(array) / sizeof(*array))

typedef struct {
	Rid var_ids[8];
	int id_cnt;
	void *up;
} Binds_part;

static int
part_holds(const Binds_part *part, const Rid id)
{
	for (; part; part = part->up)
		for (int i = 0; i < part->id_cnt; ++i)
			if (!rid_cmp(id, part->var_ids[i]))
				return 1;

	return 0;
}

/* uses more of stack over allocating memory, might want to rethink */
static ssize_t
max_binds_list(const Unfy_list *list, void *up)
{

	ssize_t len = 0;
	Binds_part part = { .up = up, .id_cnt = 0 };

	for (; list; list = list->next) {
		const Unfy_term *term = list->term;
		ssize_t sub_len;

		switch (term->type) {
		case UNFY_CONST:
		case UNFY_ORDER:
		case UNFY_IGN:
			break;
		case UNFY_LIST:
			sub_len = max_binds_list(term->u.list, &part);

			if (sub_len < 0)
				return -1;

			len += sub_len;
			break;
		case UNFY_VAR:
			if (part_holds(&part, term->u.id))
				break;

			++len;

			if (part.id_cnt <
			    (ssize_t) ARRAY_UNITS(part.var_ids)) {
				rid_set(part.var_ids[part.id_cnt], term->u.id);
				++part.id_cnt;
				break;
			}

			if ((sub_len = max_binds_list(list->next, &part)) < 0)
				return -1;

			return sub_len + len;
		}
	}

	return len;
}

static ssize_t
max_binds(const Unfy_term *term)
{
	switch (term->type) {
	case UNFY_IGN:
	case UNFY_CONST:
	case UNFY_ORDER:
		return 0;
	case UNFY_VAR:
		return 1;
	case UNFY_LIST:
		return max_binds_list(term->u.list, NULL);
	}

	/* this will never happen */
	return -1;
}

static ssize_t
bind_len(const Unfy_bind *bind)
{
	ssize_t len = 0;

	for (; bind; bind = bind->next, ++len);

	return len;
}

/* Main code */

int
rls_info_init(Rls_info *info, Unfy_term *term,
	      Rls_rule *rules, Rls_recycle *rec)
{
	info->nbind = NULL;
	info->term = term;

	if (unfy_term_revar(term, &info->nbind, &rec->unfy) < 0)
		return -1;

	if (info->nbind) {
		info->nterm = unfy_term_bind(term, info->nbind, &rec->unfy);

		if (!info->nterm)
			return -1;

		term = info->nterm;
	} else {
		info->nbind = NULL;
		info->nterm = NULL;
	}


	unfy_info_init(&info->unfy, term, rules ? rules->head : NULL);
	info->rule = rules;
	info->rsn = RLS_RSN_OKAY;
	return 0;
}

void
rls_info_dispose(Rls_info *info, Rls_recycle *rec)
{
	unfy_recycle_bind(&rec->unfy, info->nbind);
	unfy_recycle_term(&rec->unfy, info->nterm);
	unfy_info_dispose(&info->unfy, &rec->unfy);
}

void
rls_info_change(Rls_info *info, Unfy_term *term,
		Rls_rule *rules, Rls_recycle *rec)
{
	rls_info_dispose(info, rec);
	rls_info_init(info, term, rules, rec);
}

void
rls_info_next(Rls_info *info, Rls_recycle *rec)
{
	unfy_info_dispose(&info->unfy, &rec->unfy);
	info->unfy.lbind = info->unfy.rbind = NULL;
	info->rule = info->rule->next;
	info->unfy.left = info->nterm ? info->nterm : info->term;
	info->unfy.right = info->rule ? info->rule->head : NULL;
}

void
rls_recycle_init(Rls_recycle *rec)
{
	unfy_recycle_init(&rec->unfy);
	rec->rules = NULL;
	rec->srchs = NULL;
}

void
rls_recycle_empty(Rls_recycle *rec)
{
	unfy_recycle_empty(&rec->unfy);

	while (rec->rules) {
		Rls_rule *tmp = rec->rules;

		rec->rules = tmp->next;
		free(tmp);
	}

	rec->rules = NULL;

	while (rec->srchs) {
		Rls_srch *tmp = rec->srchs;

		rec->srchs = (void *) tmp->body;
		free(tmp);
	}

	rec->rules = NULL;
}

static Rls_rule *
get_rule(Rls_recycle *rec)
{
	Rls_rule *rule = rec->rules;

	if (!rule)
		return malloc(sizeof(*rule));

	rec->rules = rule->next;
	return rule;
}

void
rls_recycle_rule(Rls_recycle *rec, Rls_rule *rule,
		 Rls_dat_free dat_free, void *extra)
{
	Rls_rule *end = rule;

	if (!rule)
		return;

	while (1) {
		unfy_recycle_term(&rec->unfy, end->head);

		if (dat_free)
			dat_free(end->dat, extra);

		if (!end->actable)
			unfy_recycle_list(&rec->unfy, end->u.body);

		if (!end->next)
			break;

		end = end->next;
	}

	end->next = rec->rules;
	rec->rules = rule;

}

static Rls_rule *
rls_rule(const Rid id, Unfy_term *head, int actable, void *generic,
	 int max, Rls_rule *next, void *dat, Rls_recycle *rec)
{
	Rls_rule *rule;

	if (!(rule = get_rule(rec)))
		return NULL;

	rule->next = next;
	rule->head = head;
	rid_set(rule->id, id);
	rule->size = 0;
	rule->max_binds = max;
	rule->dat = dat;

	if ((rule->actable = actable)) {
		*(void **)(&rule->u.act) = generic;
	} else {
		Unfy_list *list = rule->u.body = generic;

		for (; list; list = list->next)
			++rule->size;
	}

	return rule;
}

static int
rls_rule_add_rule(Rls_rule **rule, const Rid id, Unfy_term *head,
		  int actable, void *generic, void *dat, Rls_recycle *rec)
{
	ssize_t lmax = max_binds(head);
	Rls_rule *here;

	if (lmax < 0)
		return -1;

	for (; *rule; rule = &(*rule)->next) {
		Unfy_info info;

		unfy_info_init(&info, head, (*rule)->head);

		switch (unfy_unify(&info, &rec->unfy)) {
		case UNFY_YES:
			if (bind_len(info.lbind) <= bind_len(info.rbind)) {
				unfy_info_dispose(&info, &rec->unfy);
				goto exit;
			}

			unfy_info_dispose(&info, &rec->unfy);
			break;
		case UNFY_NO:
			unfy_info_dispose(&info, &rec->unfy);

			if (lmax < (*rule)->max_binds)
				goto exit;

			break;
		case UNFY_ERR:
			unfy_info_dispose(&info, &rec->unfy);
			return -1;
		}
	}
exit:
	if (!(here = rls_rule(id, head, actable, generic,
			      lmax, *rule, dat, rec)))
		return -1;

	*rule = here;
	return 0;
}

int
rls_rule_add(Rls_rule **rule, const Rid id, Unfy_term *head,
	     Unfy_list *body, void *dat, Rls_recycle *rec)
{
	return rls_rule_add_rule(rule, id, head, 0, body, dat, rec);
}

int
rls_rule_add_actable(Rls_rule **rule, const Rid id, Unfy_term *head,
		     Rls_act act, void *dat, Rls_recycle *rec)
{
	return rls_rule_add_rule(rule, id, head, 1, *(void **)(&act),
				 dat, rec);
}

Rls_dif
rls_rule_same(Unfy_info *info, Rls_rule *left, Rls_rule *right,
	      Rls_recycle *rec)
{
	if (!left)
	        return right ? RLS_DIF_NULL : RLS_DIF_SAME;

	if (!right)
		return RLS_DIF_NULL;

	unfy_info_init(info, left->head, right->head);

        switch (unfy_term_same(info, &rec->unfy)) {
	case UNFY_YES:
		break;
	case UNFY_NO:
	        return RLS_DIF_HEAD;
	case UNFY_ERR:
		return RLS_DIF_ERR;
	}

	if (left->actable != right->actable) {
	        return RLS_DIF_ACTABLE;
	} else if (left->actable) {
		if (left->u.act == right->u.act)
		        goto same;

	        return RLS_DIF_ACT;
	}

	/* setting left and right NULL to represent body lists
	   since they are not stored in a term */
        info->left = NULL;
	info->right = NULL;

	switch (unfy_list_same(info, left->u.body,
			       right->u.body, &rec->unfy)) {
	case UNFY_YES:
		break;
	case UNFY_NO:
		return RLS_DIF_BODY;
	case UNFY_ERR:
		return RLS_DIF_ERR;
	}
same:
	unfy_info_dispose(info, &rec->unfy);
	return RLS_DIF_SAME;
}

Unfy_stat
rls_rule_query(Rls_info *info, Rls_recycle *rec)
{
	for (; info->rule; rls_info_next(info, rec)) {
		Unfy_stat stat = unfy_unify(&info->unfy, &rec->unfy);

		if (stat != UNFY_NO)
			return stat;

		/* info->rsn = RLS_RSN_UNFY; */
		/* return UNFY_NO; */
	}

	info->rsn = RLS_RSN_END;
	return UNFY_NO;
}

static Rls_srch *
get_srch(Rls_recycle *rec)
{
	Rls_srch *srch = rec->srchs;

	if (!srch)
		return malloc(sizeof(*srch));

	rec->srchs = (void *) srch->body;
	return srch;
}

static int
srch_init(Rls_srch **srch_ref, Rls_srch *up, Unfy_term *term,
	  Rls_rule *rules, uint16_t num, Rls_recycle *rec)
{
	if (!(*srch_ref = get_srch(rec))) {
		unfy_recycle_term(&rec->unfy, term);
		return -1;
	}

	(*srch_ref)->up = up;
	(*srch_ref)->term = term;
	(*srch_ref)->rule = rules;
	(*srch_ref)->lbind = (*srch_ref)->rbind = NULL;
	(*srch_ref)->nbind = (*srch_ref)->fbind = NULL;
        (*srch_ref)->body = NULL;
	(*srch_ref)->num = num;
	return 0;
}

static void
rec_srch_local(Rls_recycle *rec, Rls_srch *srch)
{
	if (!srch)
		return;

	unfy_recycle_term(&rec->unfy, srch->term);
	unfy_recycle_bind(&rec->unfy, srch->lbind);
	unfy_recycle_bind(&rec->unfy, srch->rbind);
	unfy_recycle_bind(&rec->unfy, srch->nbind);
	unfy_recycle_bind(&rec->unfy, srch->fbind);

	if (srch->body)
		for (int i = 0; i < srch->rule->size; ++i)
			rec_srch_local(rec, srch->body[i]);

	free(srch->body);
	srch->body = (void *) rec->srchs;
	rec->srchs = srch;
}

void
rls_recycle_srch(Rls_recycle *rec, Rls_srch *srch)
{
	if (!srch)
		return;

	for (; srch->up; srch = srch->up);

	rec_srch_local(rec, srch);
}

static Unfy_term *
rls_srch_bind(Rls_srch *srch, const Unfy_term *term, Rls_recycle *rec)
{
	Unfy_term *bound;
	Rls_srch **body = srch->body;

	if (!(bound = unfy_term_bind(term, srch->rbind, &rec->unfy)))
		return NULL;

	for (int i = 0; i < srch->rule->size && body[i]; ++i) {
		if (unfy_term_bind_set(bound, body[i]->fbind, &rec->unfy) < 0) {
			unfy_recycle_term(&rec->unfy, bound);
			return NULL;
		}
	}

	return bound;
}

static int
srch_fbind(Rls_srch *srch, Rls_recycle *rec)
{
	Unfy_bind *fbind = NULL;
	Unfy_bind *nnbind = NULL;
	Unfy_bind *nbind = srch->nbind;

	for (; nbind; nbind = nbind->next) {
		Unfy_term *bound;
		Unfy_term *term;

		if (!(bound = unfy_term_bind(nbind->term, srch->lbind, &rec->unfy))) {
			unfy_recycle_bind(&rec->unfy, fbind);
			unfy_recycle_bind(&rec->unfy, nnbind);
			return -1;
		}

		term = rls_srch_bind(srch, bound, rec);
		unfy_recycle_term(&rec->unfy, bound);

		if (!term) {
			unfy_recycle_bind(&rec->unfy, fbind);
			unfy_recycle_bind(&rec->unfy, nnbind);
			return -1;
		}

		/* it remains unchanged */
		if (term->type == UNFY_VAR &&
		    !rid_cmp(term->u.id, nbind->var_id)) {
			unfy_recycle_term(&rec->unfy, term);
			continue;
		}

		if (unfy_term_revar(term, &nnbind, &rec->unfy) < 0 ||
		    unfy_term_bind_set(term, nnbind, &rec->unfy) < 0 ||
		    unfy_bind(&fbind, nbind->var_id, term, &rec->unfy)) {
			unfy_recycle_term(&rec->unfy, term);
			unfy_recycle_bind(&rec->unfy, fbind);
			unfy_recycle_bind(&rec->unfy, nnbind);
			return -1;
		}

	}

	unfy_recycle_bind(&rec->unfy, nnbind);

	if (srch->fbind)
		unfy_recycle_bind(&rec->unfy, srch->fbind);

	srch->fbind = fbind;
	return 0;
}

static const Unfy_list *
rule_get_pos(const Rls_rule *rule, int pos)
{
	const Unfy_list *list = rule->u.body;

	for (; pos; --pos)
		list = list->next;

	return list;
}

static Rls_srch *
srch_last(Rls_srch *srch)
{
	/* down the the axioms */
	while (!srch->rule->actable && srch->body) {
		int i = 0;

		for (; i + 1 < srch->rule->size && srch->body[i + 1]; ++i);

		srch = srch->body[i];
	}

	return srch;
}

static inline Unfy_stat
srch_from(Rls_srch *srch, Rls_info *info, Rls_recycle *rec)
{
	unfy_recycle_bind(&rec->unfy, srch->lbind);
	unfy_recycle_bind(&rec->unfy, srch->rbind);
	unfy_recycle_bind(&rec->unfy, srch->nbind);
	srch->lbind = srch->rbind = srch->nbind = NULL;
	rls_info_init(info, srch->term, srch->rule, rec);

	switch (rls_rule_query(info, rec)) {
	case UNFY_YES:
		srch->rule = info->rule;
		srch->lbind = info->unfy.lbind;
		srch->rbind = info->unfy.rbind;
		srch->nbind = info->nbind;
		unfy_recycle_term(&rec->unfy, info->nterm);
		return UNFY_YES;
	case UNFY_NO:
		return UNFY_NO;
	case UNFY_ERR:
		break;
	}

	rls_info_dispose(info, rec);
	return UNFY_ERR;
}

static Unfy_stat
init_body(Rls_srch **srch_ref, Rls_recycle *rec)
{
	Unfy_term *bound;
	Rls_srch *srch = *srch_ref;

	if (!(srch->body = calloc(srch->rule->size, sizeof(Rls_srch *)))  ||
	    !(bound = rls_srch_bind(srch, srch->rule->u.body->term, rec)) ||
	    srch_init(srch->body, srch, bound, NULL, srch->num + 1, rec) < 0)
		return UNFY_ERR;

	*srch_ref = srch->body[0];
	return UNFY_YES;
}

static Unfy_stat
init_next(Rls_srch **srch_ref, Rls_srch *up, uint16_t num, Rls_recycle *rec);

static Unfy_stat
scale_up(Rls_srch **srch_ref, Rls_srch *up, uint16_t num, Rls_recycle *rec)
{
	if (srch_fbind(up, rec) < 0)
		return UNFY_ERR;

	if (!up->up) {
		*srch_ref = up;
		return UNFY_YES;
	}

	return init_next(srch_ref, up->up, num, rec);
}

static Unfy_stat
init_next(Rls_srch **srch_ref, Rls_srch *up, uint16_t num, Rls_recycle *rec)
{
	int i = 0;
	const Unfy_list *list;
	Unfy_term *bound;

	for (; i < up->rule->size && up->body[i]; ++i);

	if (i == up->rule->size)
		return scale_up(srch_ref, up, num, rec);

	list = rule_get_pos(up->rule, i);

	if (!(bound = rls_srch_bind(up, list->term, rec)) ||
	    srch_init(up->body + i, up, bound, NULL, num, rec) < 0)
		return UNFY_ERR;

	*srch_ref = up->body[i];
	return UNFY_YES;
}

static void
step_no(Rls_srch **srch_ref, Rls_recycle *rec);

static Unfy_stat
step_yes(Rls_srch **srch_ref, void *extra, Rls_recycle *rec)
{
	Rls_srch *srch = *srch_ref;

	if (!srch->rule->actable && srch->rule->u.body)
		return init_body(srch_ref, rec);

	if (srch_fbind(srch, rec) < 0)
		return UNFY_ERR;

	if (srch->rule->actable)
		switch (srch->rule->u.act(RLS_SRCH, srch, extra)) {
		case UNFY_YES:
		        break;
		case UNFY_NO:
			/* I'm lazy, this should work */
			step_no(srch_ref, rec);
			return UNFY_NO;
		case UNFY_ERR:
		        return UNFY_ERR;
		}

	if (srch->up)
		return init_next(srch_ref, srch->up, srch->num + 1, rec);

	return UNFY_YES;
}

static void
step_no(Rls_srch **srch_ref, Rls_recycle *rec)
{
	Rls_srch *up = (*srch_ref)->up;
	int i = 0;

	rec_srch_local(rec, *srch_ref);

	if (!up) {
		*srch_ref = NULL;
		return;
	}

	/* the previous srch should be last non NULL entry */
	for (; i + 1 < up->rule->size && up->body[i + 1]; ++i);

	if (!i) {
		free(up->body);
		up->body = NULL;
		*srch_ref = up;
		return;
	}

	up->body[i] = NULL;
        *srch_ref = srch_last(up->body[i - 1]);
}

static void
srch_revert(Rls_srch *srch, Rls_recycle *rec)
{
	if (srch->rule && srch->body)
		for (int i = 0; i < srch->rule->size; ++i)
			rec_srch_local(rec, srch->body[i]);

	free(srch->body);
	unfy_recycle_bind(&rec->unfy, srch->lbind);
	unfy_recycle_bind(&rec->unfy, srch->rbind);
	unfy_recycle_bind(&rec->unfy, srch->nbind);
	unfy_recycle_bind(&rec->unfy, srch->fbind);
	srch->rule = NULL;
	srch->body = NULL;
	srch->lbind = srch->rbind = srch->nbind = srch->fbind = NULL;
}

static Unfy_stat
srch_step(Rls_srch **srch_ref, Rls_rule *rules, Rls_bend bend,
	  Rls_info *info, void *extra, Rls_recycle *rec)
{
	Unfy_stat stat = UNFY_NO; /* default value for bend returning NULL */

	if ((*srch_ref)->body)
		*srch_ref = srch_last(*srch_ref);

	if (bend && !(*srch_ref)->rule) {
		Rls_rule **tmp = bend((*srch_ref)->term, &stat, extra);

		if (!tmp)
			goto check;

		rules = *tmp;
	}

	(*srch_ref)->rule = (!(*srch_ref)->rule) ? rules : (*srch_ref)->rule->next;
	stat = srch_from(*srch_ref, info, rec);
check:
	switch (stat) {
	case UNFY_YES:
		stat = step_yes(srch_ref, extra, rec);

	        if (stat == UNFY_ERR)
			break;

		return stat;
	case UNFY_NO:
		step_no(srch_ref, rec);
		return UNFY_NO;
	case UNFY_ERR:
		break;
	}

	/* Safest way to recover from error, sure we'll lose some progress, but
	 * it can be recovered in time.
	 */
	srch_revert(*srch_ref, rec);
	return UNFY_ERR;
}

static Unfy_stat
srch_loop(Rls_srch **srch_ref, Rls_rule *rules, int *limit,
	  Rls_bend bend, Rls_info *info, void *extra, Rls_recycle *rec)
{
	info->rsn = RLS_RSN_OKAY;

	while (1) {
		if (*limit > 0)
			--*limit;
		else if (!*limit) {
			if (info->rsn == RLS_RSN_OKAY) {
				/* makes safe for disposing info */
				info->rsn = RLS_RSN_LIMIT;
				info->nbind = NULL;
				info->nterm = NULL;
				info->unfy.lbind = info->unfy.rbind = NULL;
			}

			return UNFY_NO;
		}

		if (info->rsn != RLS_RSN_OKAY)  {
			rls_info_dispose(info, rec);
			info->rsn = RLS_RSN_OKAY;
		}

		switch (srch_step(srch_ref, rules, bend,
				  info, extra, rec)) {
		case UNFY_YES:
			if (!(*srch_ref)->up)
				return UNFY_YES;

			continue;
		case UNFY_NO:
			if (!(*srch_ref))
				return UNFY_NO;

			continue;
		case UNFY_ERR:
			return UNFY_ERR;
		}
	 }

	return UNFY_ERR;
}

Unfy_stat
rls_srch_limit(Rls_srch **srch_ref, Unfy_term *term, Rls_rule *rules,
	       int *limit, Rls_bend bend, Rls_info *info, void *extra,
	       Rls_recycle *rec)
{
	if (!*srch_ref && srch_init(srch_ref, NULL, term, NULL, 0, rec) < 0)
		return UNFY_ERR;

	return srch_loop(srch_ref, rules, limit, bend, info, extra, rec);
}

Unfy_stat
rls_srch(Rls_srch **srch_ref, Unfy_term *term, Rls_rule *rules,
	 Rls_bend bend, Rls_info *info, void *extra, Rls_recycle *rec)
{
	int limit = -1;

	return rls_srch_limit(srch_ref, term, rules, &limit,
			      bend, info, extra, rec);
}

void
rls_srch_next(Rls_srch **srch)
{
	Rls_srch *tmp;

	if (!*srch)
		return;

	if ((*srch)->rule->size) {
		*srch = *(*srch)->body;
		return;
	}

	tmp = *srch;

	while ((*srch = (*srch)->up)) {
		uint16_t i = 0;

		for (; (*srch)->body[i] != tmp; ++i);

		if (i + 1 < (*srch)->rule->size) {
			*srch = (*srch)->body[i + 1];
			return;
		}

		tmp = *srch;
	}
}

int
rls_srch_same_next(Rls_srch **left, Rls_srch **right)
{
	Rls_srch *left_up;
	Rls_srch *right_up;

	if ((*left)->rule->size) {
		*left = *(*left)->body;
		*right = *(*right)->body;
		return 1;
	}

	for (;; *left = left_up, *right = right_up) {
		uint16_t i = 0;

	        left_up = (*left)->up;
	        right_up = (*right)->up;

		if (!left_up)
			return 0;

		for (; left_up->body[i] != *left; ++i);

		if (i + 1 < left_up->rule->size) {
			*left = left_up->body[i + 1];
			*right = right_up->body[i + 1];
			return 1;
		}
	}
}

Rls_dif
rls_srch_same(Unfy_info *info, Rls_srch **left, Rls_srch **right,
	      Rls_recycle *rec)
{
	Rls_dif dif;

	if (!*left)
		return !*right ? RLS_DIF_SAME : RLS_DIF_NULL;

        if (!*right)
		return RLS_DIF_NULL;

	do {
		if ((dif = rls_rule_same(info, (*left)->rule,
					 (*right)->rule, rec)) != RLS_DIF_SAME)
			return dif;
	} while (rls_srch_same_next(left, right));

	return RLS_DIF_SAME;
}

Unfy_stat
rls_srch_run(Rls_srch *srch, void *extra)
{
	Unfy_stat stat = UNFY_YES;

	if (!srch)
		return UNFY_YES;

	if (srch->rule->actable)
		return srch->rule->u.act(RLS_RUN, srch, extra);

	for (int i = 0; i < srch->rule->size; ++i)
		if ((stat = rls_srch_run(srch->body[i], extra)) != UNFY_YES)
			break;

	return stat;
}
